﻿using Library.Collections.Generic;
using Library.Linq;
using Library.Linq.Expressions;
using Library.Logic.Constraints;
using Library.Logic.Inference;
using Library.Logic.Unification;
using System;
using System.Linq.Expressions;
using TRULE = System.Linq.Expressions.Expression<System.Func<System.Linq.IQueryable<System.Linq.Expressions.Expression>, System.Collections.Generic.IEnumerable<System.Collections.Generic.IEnumerable<System.Linq.Expressions.Expression>>>>;
using TEXPRESSION = System.Linq.Expressions.Expression;

namespace Library.Logic
{
    public static partial class Builtin
    {
        static Expression _true = Expression.Constant(true, typeof(bool));
        static Expression _false = Expression.Constant(false, typeof(bool));

        public static Expression True { get { return _true; } }
        public static Expression False { get { return _false; } }

        public static Set Universal { get { throw new NotImplementedException(); } }
        public static Set Empty { get { throw new NotImplementedException(); } }

        static Expression GetExpression(object value)
        {
            Expression expr = value as Expression;

            throw new NotImplementedException();
        }

        public static ISetReadOnly Complement(this ISetReadOnly set, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            return set.Provider.CreateSet(Complement(set.ElementConstraints, reasoner));
        }
        public static ISetReadOnly Complement(this ISetReadOnly set, ISetReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            return set.Provider.CreateSet(Complement(set.ElementConstraints, other.ElementConstraints, reasoner));
        }
        public static ISetReadOnly Intersect(this ISetReadOnly set, ISetReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            return set.Provider.CreateSet(Intersect(set.ElementConstraints, other.ElementConstraints, reasoner));
        }
        public static ISetReadOnly Union(this ISetReadOnly set, ISetReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            return set.Provider.CreateSet(Union(set.ElementConstraints, other.ElementConstraints, reasoner));
        }

        public static IConstraintsReasonReadOnly Complement(this IConstraintsReasonReadOnly constraints, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            throw new NotImplementedException();
        }
        public static IConstraintsReasonReadOnly Complement(this IConstraintsReasonReadOnly constraints, IConstraintsReasonReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            throw new NotImplementedException();
        }
        public static IConstraintsReasonReadOnly Intersect(this IConstraintsReasonReadOnly constraints, IConstraintsReasonReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            throw new NotImplementedException();
        }
        public static IConstraintsReasonReadOnly Union(this IConstraintsReasonReadOnly constraints, IConstraintsReasonReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner)
        {
            throw new NotImplementedException();
        }

        //public static IConstraintsReadOnly<TDelegate> Complement<TDelegate>(this IConstraintsReadOnly<TDelegate> constraints, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}
        //public static IConstraintsReadOnly<TDelegate> Intersect<TDelegate>(this IConstraintsReadOnly<TDelegate> constraints, IConstraintsReadOnly<TDelegate> other, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}
        //public static IConstraintsReadOnly<TDelegate> Union<TDelegate>(this IConstraintsReadOnly<TDelegate> constraints, IConstraintsReadOnly<TDelegate> other, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}

        //public static IConstraints Complement(this IConstraints constraints, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}
        //public static IConstraints Intersect(this IConstraints constraints, IConstraintsReadOnly other, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}
        //public static IConstraints Union(this IConstraints constraints, IConstraintsReadOnly other, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}

        //public static IConstraints<TDelegate> Complement<TDelegate>(this IConstraints<TDelegate> constraints, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}
        //public static IConstraints<TDelegate> Intersect<TDelegate>(this IConstraints<TDelegate> constraints, IConstraintsReadOnly<TDelegate> other, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}
        //public static IConstraints<TDelegate> Union<TDelegate>(this IConstraints<TDelegate> constraints, IConstraintsReadOnly<TDelegate> other, IReasonerReadOnly<Expression> reasoner)
        //{
        //    throw new NotImplementedException();
        //}

        public static bool IsProperSubsetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool IsProperSupersetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool IsSubsetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool IsSupersetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool Equals(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }

        public static bool IsProperSubsetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }
        public static bool IsProperSupersetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }
        public static bool IsSubsetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }
        public static bool IsSupersetOf(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }
        public static bool Equals(this IHasElementConstraintsReadOnly set, IHasElementConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }

        public static bool Equals(this IConstraintsReadOnly constraints, IConstraintsReadOnly other, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool Equals(this IConstraintsReasonReadOnly constraints, IConstraintsReasonReadOnly other, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }

        public static bool CanAdd(this IConstraints constraints, TEXPRESSION constraint, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            if (constraints.Contains(constraint)) return false;
            return !reasoner.Reason(constraints.Concat(constraint)).Contains(_false);
        }
        public static bool CanRemove(this IConstraints constraints, TEXPRESSION constraint, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool CanAdd(this IConstraintsReason constraints, TEXPRESSION constraint, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            if (constraints.Contains(constraint))
            {
                argument = Builtin.Inference();
                return false;
            }
            return !reasoner.Reason(constraints.Concat(constraint)).Contains(_false, out argument);
        }
        public static bool CanRemove(this IConstraintsReason constraints, TEXPRESSION constraint, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            if (!constraints.Contains(constraint))
            {
                argument = Builtin.Inference();
                return false;
            }
            return !reasoner.Reason(constraints.Except(constraint)).Contains(_false, out argument);
        }

        public static bool CanUnify(this IHasConstraintsReadOnly obj, object[] value)
        {
            if (obj == null) throw new ArgumentNullException("obj");
            IUnifiableReadOnly unifiable = obj as IUnifiableReadOnly;
            if (unifiable != null)
            {
                return unifiable.CanUnify(value);
            }
            else
            {
                return obj.Constraints.Validate(value);
            }
        }
        public static bool CanUnify(this IHasConstraintsReadOnly obj, object[] value, IMapCollection<VariableExpression, object[]> mappings)
        {
            if (obj == null) throw new ArgumentNullException("obj");
            IUnifiableReadOnly unifiable = obj as IUnifiableReadOnly;
            if (unifiable != null)
            {
                return unifiable.CanUnify(value, mappings);
            }
            throw new NotImplementedException();
        }
        public static bool CanUnify(this IHasConstraintsReasonReadOnly obj, object[] value, out IInference argument)
        {
            if (obj == null) throw new ArgumentNullException("obj");
            IUnifiableReasonReadOnly unifiable = obj as IUnifiableReasonReadOnly;
            if (unifiable != null)
            {
                return unifiable.CanUnify(value, out argument);
            }
            else
            {
                return obj.Constraints.Validate(value, out argument);
            }
        }
        public static bool CanUnify(this IHasConstraintsReasonReadOnly obj, object[] value, IMapCollection<VariableExpression, object[]> mappings, out IInference argument)
        {
            if (obj == null) throw new ArgumentNullException("obj");
            IUnifiableReasonReadOnly unifiable = obj as IUnifiableReasonReadOnly;
            if (unifiable != null)
            {
                return unifiable.CanUnify(value, mappings, out argument);
            }
            throw new NotImplementedException();
        }

        public static bool Unify(this IHasConstraints obj, object[] value)
        {
            throw new NotImplementedException();
        }
        public static bool Unify(this IHasConstraintsReason obj, object[] value, out IInference argument)
        {
            throw new NotImplementedException();
        }



        //public static bool EnsureEntails<X, T>(this X obj, T item, IReasoner<T> reasoner)
        //    where X : System.Linq.IQueryable<T>, Library.Collections.Generic.ICollection<T>
        //{
        //    if (reasoner.Reason(obj).Contains(item)) return true;
        //    return obj.Add(item);
        //}

        //public static ITransaction<bool> EnsureEntails<X, T>(this X obj, T item, IReasoner<T> reasoner)
        // where X : System.Linq.IQueryable<T>, Library.Collections.Specialized.ICollectionTransactionable<T>
        //{
        //    if (reasoner.Reason(obj).Contains(item)) return Scope.True;
        //    return obj.Add(item);
        //}

        public static bool EnsureEntails(this IConstraints obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            if (reasoner.Reason(obj).Contains(expression)) return true;
            return obj.Add(expression);
        }



        public static bool Exists(this IHasConstraintsReadOnly obj, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            return !reasoner.Reason(obj.Constraints).Contains(_false);
        }
        public static bool Exists(this IHasConstraintsReadOnly obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            return !reasoner.Reason(obj.Constraints).Contains(Expression.Not(expression));
        }
        public static bool Exists(this IHasConstraintsReadOnly obj, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            return !reasoner.Reason(obj.Constraints).Contains(_false, out argument);
        }
        public static bool Exists(this IHasConstraintsReadOnly obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            return !reasoner.Reason(obj.Constraints).Contains(Expression.Not(expression), out argument);
        }
        //public static bool Exists(this IReasoner<Expression> reasoner, IHasConstraintsReadOnly x)
        //{
        //    return !reasoner.Reason(x.Constraints).Contains(_false);
        //}
        //public static bool Exists(this IReasoner<Expression> reasoner, IHasConstraintsReadOnly x, Expression expression)
        //{
        //    return !reasoner.Reason(x.Constraints).Contains(Expression.Not(expression));
        //}

        //Uniqueness quantification can be expressed in terms of the existential and universal quantifiers of predicate logic by defining the formula ∃!x P(x) to mean
        
        //    \exists x\, P(x) \wedge \neg \exists x,y \, ( P(x) \wedge P(y) \wedge (x \neq y)),

        //or equivalently,
        
        //    \exists x \, ( P(x) \wedge \forall y\,(P(y) \to x = y)).
        //An equivalent definition that has the virtue of separating the notions of existence and uniqueness into two clauses, at the expense of brevity, is
        
        //    \exists x\, P(x) \wedge \forall y\, \forall z\,((P(y) \wedge P(z)) \to y = z).
        
        //Another equivalent definition with the advantage of brevity is
            
        //    \exists x\,\forall y\,(P(y) \leftrightarrow x = y).

        public static bool Unique(this IHasConstraintsReadOnly obj, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool Unique(this IHasConstraintsReadOnly obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            throw new NotImplementedException();
        }
        public static bool Unique(this IHasConstraintsReadOnly obj, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }
        public static bool Unique(this IHasConstraintsReadOnly obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            throw new NotImplementedException();
        }

        //public static bool Unique(this IReasoner<Expression> reasoner, IHasConstraintsReadOnly x)
        //{
        //    throw new NotImplementedException();
        //}
        //public static bool Unique(this IReasoner<Expression> reasoner, IHasConstraintsReadOnly x, Expression expression)
        //{
        //    throw new NotImplementedException();
        //}

        public static bool ForAll(this IHasConstraintsReadOnly obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION> reasoner)
        {
            return reasoner.Reason(obj.Constraints).Contains(expression);
        }
        public static bool ForAll(this IHasConstraintsReadOnly obj, TEXPRESSION expression, IReasonerReadOnly<TEXPRESSION, TRULE> reasoner, out IInference argument)
        {
            return reasoner.Reason(obj.Constraints).Contains(expression, out argument);
        }       
        //public static bool ForAll(this IReasoner<Expression> reasoner, IHasConstraintsReadOnly x, Expression expression)
        //{
        //    return reasoner.Reason(x.Constraints).Contains(expression);            
        //}

        //public static IReasoner<Expression> Reasoner
        //{
        //    get;
        //    set;
        //}



        public static IInference Inference()
        {
            throw new NotImplementedException();
        }



        public static Variable CreateVariable(this IHasElementConstraintsReasonReadOnly set)
        {
            throw new NotImplementedException();
        }

        public static Variable CreateVariable(this Type type)
        {
            throw new NotImplementedException();
        }
    }
}
